This invention relates generally to analysis of circuit designs, and more particularly to generating properties for circuit designs.
As the complexity in circuit design has increased, there has been a corresponding improvement in various kinds of verification and debugging techniques. In fact, these verification and debugging techniques have evolved from relatively simple transistor circuit-level simulation (in the early 1970s) to logic gate-level simulation (in the late 1980s) to the current art that uses Register Transfer Language (RTL)-level simulation, and formal verification. RTL describes the registers of a computer or digital electronic system and the way in which data are transferred among the combinational logic between registers.
During some of these verification techniques, a circuit design may be tested against a set of properties to evaluate the operation of the circuit design. Properties are logical statements that describe some aspect of the circuit design. The conventional method for creating properties requires the circuit designer to examine the circuit design and to manually code the properties based on the circuit designer's own knowledge of the circuit design. However, manually creating properties is tedious and prone to errors. Furthermore, as the circuit design changes, the properties must be checked for consistency and re-written to comply with the design changes. Accordingly, what are needed are techniques to expedite the process of generating properties and to reduce the overall time needed for verifying a circuit design.